@gebner This is great. Thanks for working on this. I didn't have time to review it yet. BTW, the PR is currently marked as a draft, is something missing?
Could you please copy some of the comments above as docstrigs? For example, the inherited text could be copied as a docstring for registerTraceClass.

!bench

Here are the benchmark results for commit f722465.
There were significant changes against commit 860d726:

  Benchmark     Metric    Change
  ==============================
+ stdlib size   lines C      -1%

This is awesome! Could you comment on whether there is a clear path to implementing Daniel's proposal later as well?

This is awesome! Could you comment on whether there is a clear path to implementing Daniel's proposal later as well?

Is it possible to implement something like Daniel suggested (if I understand it correctly, a set_option trace.inside.Meta.isDefEq true that enables all trace messages inside a Meta.isDefEq node)? Certainly. But that would also enable a lot of junk trace messages as well, so I'm not sure how useful such a blanket setting would be.

Is it possible to implement something like Daniel suggested (if I understand it correctly, a set_option trace.inside.Meta.isDefEq true that enables all trace messages inside a Meta.isDefEq node)? Certainly. But that would also enable a lot of junk trace messages as well, so I'm not sure how useful such a blanket setting would be

Probably not much, but the suggestion of composable filters would be extremely useful:

One might want the Meta.synthInstance.newSubgoal calls that occur inside isDefEq calls.

With the trace explorer, the ideal UI might be something like a fuzzy search input box where we can type in isDefEq Meta.synthInstance.newSubgoal (think CSS selectors) and have the trace tree auto-expand to show those. It would either need server support so that we don't have to eagerly toInteractive the entire trace, or we could send just a "trace outline" containing only the classes but not the messages and have the client filter that.

It would either need server support so that we don't have to eagerly toInteractive the entire trace, or we could send just a "trace outline" containing only the classes but not the messages and have the client filter that.

Any thoughts on what the ideal RPC API for that would be? With this PR there's only a LazyTraceChildren type, so even if we add an RPC call like searchTraceChildren{ children: LazyTraceChildren, query: String }: SearchResult we'd still need to do half of the search on the client (since we only have an RPC reference for the kids, but not the root node). On the other hand, I didn't want to hide the root node behind an RPC ref, because that would require additional round-trips.

Specifying the filters on the Lean side is much easier of course, and requires less API work. Something like enable_trace isDefEq>synthInstance in def ... would be fairly straightforward to implement.

BTW, the PR is currently marked as a draft, is something missing?

I wanted some discussion on the RPC API first (see exchange with Wojciech). There's also plenty of trace messages to change so that they fit better into the new concept. The only module I've really touched is the TC synthesizer, the rest is just the minimum to get rid of traceCtx and withNestedTraces. But I can also do that in follow-up PRs.

It looks like this could also serve as the basis for a metaprogram that essentially tests a trace against a spec, right? The idea here is that I'd like to step through some instance searches in Functional Programming in Lean to help readers get an idea of how outParam and defaultInstance affect the process, but this is only tenable to keep up to date if I can test the resulting text against what Lean is actually doing. It seems that enabling the right traces, capturing them, and then validating them could be doable with this new .trace constructor, right?

Any thoughts on what the ideal RPC API for that would be?

Sadly no, you probably have a better idea of it by now.

Specifying the filters on the Lean side is much easier of course, and requires less API work. Something like enable_trace isDefEq>synthInstance in def ... would be fairly straightforward to implement.

The tradeoff seems to be:

• If we send a trace outline, we could have a nice quickly-responsive UI with a fuzzy search box. But implementation effort is duplicated across infoview/NVim.
• If we use an enable_trace command, the server does everything and no changes to clients may be required thanks to the collapseByDefault flag which we can just toggle appropriately. If done the obvious way though, there will be a pretty bad interaction with long-running commands which produce huge traces in that changing the enable_trace will re-elaborate the entire snapshot of the command below. So quick searching of the trace would not really work.

Thinking about the search API issue a bit more, I believe that all searching should happen server-side. This is great because:

• It also works on the command-line.
• Filters can be shared in snippets on Zulip.
• It reduces code duplication in editors.
• The content of the traces can be searched as well. For example, we can show all type-class traces with metavariables in them, etc.

We can implement this without breaking backwards compatibility by adding an additional field to the MsgEmbed for traces, namely WithRpcRef MessageData for the .trace object itself (maybe with indentation and naming contexts etc.). Then we only need to add an RPC call searchTrace{trace: MessageData, query: String}: MessageData and hook it up in the editors.

It looks like this could also serve as the basis for a metaprogram that essentially tests a trace against a spec, right? The idea here is that I'd like to step through some instance searches in Functional Programming in Lean to help readers get an idea of how outParam and defaultInstance affect the process, but this is only tenable to keep up to date if I can test the resulting text against what Lean is actually doing. It seems that enabling the right traces, capturing them, and then validating them could be doable with this new .trace constructor, right?

@david-christiansen Indeed, what you describe is a bit easier now since there is a structured trace representation so you don't need to search for the regex \[([^]+)\] (.*) in the diagnostic to find traces. The trace messages are however completely free-form, you still need string processing to check if ✅ apply I2 to R A C is the expected output or not.

The trace messages are also not stable, and will be improved over time.

I've changed the serialization of trace to an object to make easier to extend in the future. See comment above about server-side search.

Being unstable and improved over time seems to be a common feature of Lean 4 :-) Thanks!